Model Checking
--------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Logic](../Logic/README.md#logic), [Formal Specification](../Formal%20Specification/README.md#formal-specification), [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving), [TLA(plus)](../TLA(plus)/README.md#tlaplus)_

- - - -


### Web resources

[Alloy (specification language) - Wikipedia](https://en.wikipedia.org/wiki/Alloy_(specification_language))

[multi tasking - Help understanding Petersons Algorithm for N Processes - Computer Science Stack Exchange](https://cs.stackexchange.com/questions/164777/help-understanding-petersons-algorithm-for-n-processes) ★ [💭](commentary/Chris%20Pressey.md#multi-tasking---help-understanding-petersons-algorithm-for-n-processes---computer-science-stack-exchange)

[Sally by SRI-CSL](https://sri-csl.github.io/sally/) ★

[The Omega Library Interface Guide](https://www.cs.umd.edu/projects/omega/interface_doc/interface.html) ★

[Getting started with SMV](https://santos.cs.ksu.edu/smv-doc/tutorial/tutorial.html) ★


### Repositories

_(in [x86](../x86/README.md#x86))_ [zwegner/x86-sat: Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs](https://github.com/zwegner/x86-sat) ★★★


### Papers

[Lecture Notes on CTL Model Checking](https://www.cs.cmu.edu/~15414/s23/s22/lectures/23-ctl.pdf) ★

[Model Checking CTL is Almost Always Inherently Sequential](https://arxiv.org/abs/1103.4990) [💭](commentary/Chris%20Pressey.md#model-checking-ctl-is-almost-always-inherently-sequential)

[Cycle Detection in Computation Tree Logic](https://arxiv.org/abs/1609.04095) ★ [💭](commentary/Chris%20Pressey.md#cycle-detection-in-computation-tree-logic)

[Direct Model-checking of SysML Models](https://www.scitepress.org/Papers/2021/102563/102563.pdf) ★ [💭](commentary/Chris%20Pressey.md#direct-model-checking-of-sysml-models)

_(in [Modal Logic](../Modal%20Logic/README.md#modal-logic))_ Modal Mu-Calculi (online @ [www.julianbradfield.org](https://www.julianbradfield.org/Research/MLH-bradstir.pdf)) [💭](commentary/Chris%20Pressey.md#modal-mu-calculi)

_(in [Software Engineering](../Software%20Engineering/README.md#software-engineering))_ Use of Formal Methods at Amazon Web Services (online @ [lamport.azurewebsites.net](https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#use-of-formal-methods-at-amazon-web-services)